fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)
↳ QTRS
↳ DependencyPairsProof
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)
IF_9(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, in_2, st_2, tail(in_3), st_3, m)
IF_5(st_1, in_2, st_2, in_3, st_3, m, true) → TAIL(in_2)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(map_f(two, head(in_2)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
RING(st_1, in_2, st_2, in_3, st_3, m) → LEQ(m, length(st_2))
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → FSTSPLIT(m, st_3)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, st_1)
RING(st_1, in_2, st_2, in_3, st_3, m) → HEAD(in_2)
IF_9(st_1, in_2, st_2, in_3, st_3, m, true) → TAIL(in_3)
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(three, head(in_3))
LENGTH(cons(h, t)) → LENGTH(t)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(three, head(in_3))
IF_5(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, tail(in_2), st_2, in_3, st_3, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
RING(st_1, in_2, st_2, in_3, st_3, m) → LENGTH(st_3)
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(two, head(in_2)), st_2)
IF_7(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → IF_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
MAP_F(pid, cons(h, t)) → APP(f(pid, h), map_f(pid, t))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → EMPTY(fstsplit(m, app(map_f(two, head(in_2)), st_2)))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(three, head(in_3)), st_3)
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → IF_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(three, head(in_3)), st_3))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_2)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(three, head(in_3)), st_3)
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(map_f(three, head(in_3)))
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → IF_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, app(map_f(three, head(in_3)), st_3))
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, st_2)
APP(cons(h, t), x) → APP(t, x)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_2)
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → FSTSPLIT(m, st_2)
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(two, head(in_2))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(two, head(in_2)), st_2)
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_1)
LEQ(s(n), s(m)) → LEQ(n, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → LEQ(m, length(st_3))
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → TAIL(in_2)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → EMPTY(fstsplit(m, app(map_f(three, head(in_3)), st_3)))
RING(st_1, in_2, st_2, in_3, st_3, m) → FSTSPLIT(m, st_1)
RING(st_1, in_2, st_2, in_3, st_3, m) → MAP_F(two, head(in_2))
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → EMPTY(fstsplit(m, st_3))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(two, head(in_2)), st_2))
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_2)
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → TAIL(in_3)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(two, head(in_2)), st_2))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
RING(st_1, in_2, st_2, in_3, st_3, m) → LENGTH(st_2)
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(fstsplit(m, st_1))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → IF_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
RING(st_1, in_2, st_2, in_3, st_3, m) → MAP_F(three, head(in_3))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_3)
FSTSPLIT(s(n), cons(h, t)) → FSTSPLIT(n, t)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, app(map_f(two, head(in_2)), st_2))
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → EMPTY(fstsplit(m, st_2))
MAP_F(pid, cons(h, t)) → MAP_F(pid, t)
RING(st_1, in_2, st_2, in_3, st_3, m) → HEAD(in_3)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_3)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(two, head(in_2))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → RING(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
SNDSPLIT(s(n), cons(h, t)) → SNDSPLIT(n, t)
IF_7(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_3)
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
IF_9(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, in_2, st_2, tail(in_3), st_3, m)
IF_5(st_1, in_2, st_2, in_3, st_3, m, true) → TAIL(in_2)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(map_f(two, head(in_2)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
RING(st_1, in_2, st_2, in_3, st_3, m) → LEQ(m, length(st_2))
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → FSTSPLIT(m, st_3)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, st_1)
RING(st_1, in_2, st_2, in_3, st_3, m) → HEAD(in_2)
IF_9(st_1, in_2, st_2, in_3, st_3, m, true) → TAIL(in_3)
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(three, head(in_3))
LENGTH(cons(h, t)) → LENGTH(t)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(three, head(in_3))
IF_5(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, tail(in_2), st_2, in_3, st_3, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
RING(st_1, in_2, st_2, in_3, st_3, m) → LENGTH(st_3)
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(two, head(in_2)), st_2)
IF_7(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → IF_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
MAP_F(pid, cons(h, t)) → APP(f(pid, h), map_f(pid, t))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → EMPTY(fstsplit(m, app(map_f(two, head(in_2)), st_2)))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(three, head(in_3)), st_3)
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → IF_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(three, head(in_3)), st_3))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_2)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(three, head(in_3)), st_3)
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(map_f(three, head(in_3)))
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → IF_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, app(map_f(three, head(in_3)), st_3))
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, st_2)
APP(cons(h, t), x) → APP(t, x)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_2)
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → FSTSPLIT(m, st_2)
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(two, head(in_2))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(two, head(in_2)), st_2)
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_1)
LEQ(s(n), s(m)) → LEQ(n, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → LEQ(m, length(st_3))
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → TAIL(in_2)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → EMPTY(fstsplit(m, app(map_f(three, head(in_3)), st_3)))
RING(st_1, in_2, st_2, in_3, st_3, m) → FSTSPLIT(m, st_1)
RING(st_1, in_2, st_2, in_3, st_3, m) → MAP_F(two, head(in_2))
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → EMPTY(fstsplit(m, st_3))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(two, head(in_2)), st_2))
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_2)
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → TAIL(in_3)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(two, head(in_2)), st_2))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
RING(st_1, in_2, st_2, in_3, st_3, m) → LENGTH(st_2)
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(fstsplit(m, st_1))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → IF_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
RING(st_1, in_2, st_2, in_3, st_3, m) → MAP_F(three, head(in_3))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_3)
FSTSPLIT(s(n), cons(h, t)) → FSTSPLIT(n, t)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, app(map_f(two, head(in_2)), st_2))
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → EMPTY(fstsplit(m, st_2))
MAP_F(pid, cons(h, t)) → MAP_F(pid, t)
RING(st_1, in_2, st_2, in_3, st_3, m) → HEAD(in_3)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_3)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(two, head(in_2))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → RING(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
SNDSPLIT(s(n), cons(h, t)) → SNDSPLIT(n, t)
IF_7(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_3)
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
APP(cons(h, t), x) → APP(t, x)
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP(cons(h, t), x) → APP(t, x)
The value of delta used in the strict ordering is 1/2.
POL(APP(x1, x2)) = (2)x_1
POL(cons(x1, x2)) = 1/4 + (7/2)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
MAP_F(pid, cons(h, t)) → MAP_F(pid, t)
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MAP_F(pid, cons(h, t)) → MAP_F(pid, t)
The value of delta used in the strict ordering is 1/2.
POL(cons(x1, x2)) = 1/4 + (7/2)x_2
POL(MAP_F(x1, x2)) = (2)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LENGTH(cons(h, t)) → LENGTH(t)
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LENGTH(cons(h, t)) → LENGTH(t)
The value of delta used in the strict ordering is 1/2.
POL(LENGTH(x1)) = (2)x_1
POL(cons(x1, x2)) = 1/4 + (7/2)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
LEQ(s(n), s(m)) → LEQ(n, m)
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LEQ(s(n), s(m)) → LEQ(n, m)
The value of delta used in the strict ordering is 15/8.
POL(LEQ(x1, x2)) = (15/4)x_2
POL(s(x1)) = 1/2 + (13/4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
SNDSPLIT(s(n), cons(h, t)) → SNDSPLIT(n, t)
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
SNDSPLIT(s(n), cons(h, t)) → SNDSPLIT(n, t)
The value of delta used in the strict ordering is 1/8.
POL(cons(x1, x2)) = (13/4)x_2
POL(SNDSPLIT(x1, x2)) = (1/2)x_1 + (15/4)x_2
POL(s(x1)) = 1/4 + (9/4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
FSTSPLIT(s(n), cons(h, t)) → FSTSPLIT(n, t)
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FSTSPLIT(s(n), cons(h, t)) → FSTSPLIT(n, t)
The value of delta used in the strict ordering is 1/8.
POL(cons(x1, x2)) = (13/4)x_2
POL(s(x1)) = 1/4 + (9/4)x_1
POL(FSTSPLIT(x1, x2)) = (1/2)x_1 + (15/4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → IF_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
IF_9(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, in_2, st_2, tail(in_3), st_3, m)
IF_5(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, tail(in_2), st_2, in_3, st_3, m)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → IF_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → IF_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
IF_7(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → IF_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → RING(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)